Computer software development has proven a challenging engineering task. Computer software may require millions of hours to develop, costing billions of dollars. Despite these efforts, program errors, or bugs, are inevitably introduced into computer code during software development. In fact, many software development companies employ software testers whose sole purpose is to identify and catalogue these program errors. Unfortunately, manual software testing performed by human software testers is expensive, and only results in the testing of code paths that are actually executed by the software testers.
In addition to manual testing, software engineers attempt to identify program errors by including tests in the program code itself. One technique is to define invariant conditions that should always be true at a given point in the program code. If an invariant condition is ever false, then a program error exists. During testing and debugging phases of software development (that is, before the software has been distributed to end users), the use of invariant conditions within program code may enable testers and developers to identify program errors that would otherwise go undetected.
In practice, program invariants are defined by assert statements that contain programming expressions. Other types of program invariants, such as assume statements, are similarly used. The programming expressions may comprise functions and variables defined in the program and, as such, the assert statements may directly investigate the state of the program. At runtime these assert statements are evaluated in the context of the code as it is executing. While assert statements may validate the state of the program every time the program is executed, assert statements only validate expressions in the context of the code paths that are actually executed. Code paths that are not executed are not validated by assert statements, and therefore may contain program errors. These program errors may then manifest themselves when a customer invokes an untested code path, leading to data corruption or data loss.